from z3 import *

Tie, Shirt = Bools("Tie Shirt")
s = Solver()
s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))

# 判断是否满足
print(s.check())
# sat

# 输出满足的模型
print(s.model())
# [Tie = False, Shirt = True]
